CS60030 Formal Systems | SPRING 2023, L-T-P: 3-1-0 |
Schedule
Instructor Prof. Pallab Dasgupta
Timing Wed 10:00 -11:00
Thu 9:00 - 10:00
Fri 11:00 - 13:00Venue CSE Room No: 108 Teaching Assistants Sourav Das (sourav.iniesta13@gmail.com),
Briti Gangopadhay (briti.tana@gmail.com)
Syllabus
- Introduction
- Succinct Representations
- Symbolic Reachability
- Specification Formalisms
- Omega Regular Languages and Buchi Automata
- Model Checking
- Scalability in Model Checking
- Program Verification
- Timed Automata
- Hybrid Automata
Books and References
[1] Pallab Dasgupta A Roadmap for Formal Property Verification, Springer, 2006 [2] Christel Baier and Joost-Pieter Katoen Principles of Model Checking, MIT Press, 2008. [3] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem Handbook of Model Checking, Springer, 2019 [4] Rajeev Alur Principles of Cyber-Physical Systems, MIT Press, 2015 Online Material
Week Topic Chapter Tutorial Week 1 Introduction Introduction Introduction Succinct Representations Succinct Representations Succinct Representations Week 2 Symbolic Reachability Symbolic Reachability Symbolic Reachability Week 3 Hands on SAT Hands on SAT - Tutorial SAT Tutorial SAT and BDD Tutorial SAT and BDD - Tutorial SAT and BDD Week 4 Omega Regular Languages and Buchi Automata Omega Regular Languages and Buchi Automata Omega Regular Languages and Buchi Automata Week 5 Tutorial on Symbolic Reachability and Omega Regular Languages Tutorial on Symbolic Reachability and Omega Regular Languages - Tutorial on Symbolic Reachability and Omega Regular Languages Week 6 Specification Formalisms Specification Formalisms Specification Formalisms - Week 7 Model Checking Model Checking Model Checking Tutorial 4 LTL, CTL and Model Checking - Tutorial on LTL, CTL and Model Checking Week 8 Scalability in Model Checking Scalability in Model Checking Scalability in Model Checking Program Verification Program Verification Program Verification Week 9 Bounded Model Checking Bounded Model Checking Bounded Model Checking Induction Interpolation PDR Induction Interpolation PDR Induction Interpolation PDR Week 10 Timed Automata Timed Automata Timed Automata Week 11 Tutorial TIMED AUTOMATA & HYBRID SYSTEMS Tutorial: Timed Automata & Hybrid Systems Week 12 Hybrid Automata Hybrid Automata Hybrid Automata Previous course pages: 2021 | 2020 | 2019
CS60030 Formal Systems | Spring 2023, L-T-P: 3-1-0 |